$\forall$$A$, $T$:Type, $L$:$T$ List, $k$:$A$, $i$:$\mathbb{N}$, $f$:($T$$\rightarrow$\{$i$..($i$+$\parallel$$L$$\parallel$)$^{-}$\}$\rightarrow$$A$$\rightarrow$$A$).
\\[0ex]reduce2($f$;$k$;$i$;$L$) $=$ reduce2($\lambda$$x$,$i$,$l$. $f$($x$,$i$$-$1,$l$);$k$;$i$+1;$L$) $\in$ $A$